Problem: f(f(a())) -> c(n__f(n__g(n__f(n__a())))) f(X) -> n__f(X) g(X) -> n__g(X) a() -> n__a() activate(n__f(X)) -> f(activate(X)) activate(n__g(X)) -> g(activate(X)) activate(n__a()) -> a() activate(X) -> X Proof: Bounds Processor: bound: 2 enrichment: match automaton: final states: {8,7,6,5} transitions: a1() -> 65* g1(63) -> 64* activate1(55) -> 56* activate1(57) -> 58* activate1(49) -> 50* activate1(46) -> 47* f1(47) -> 48* n__a1() -> 41* n__g1(25) -> 26* n__g1(39) -> 40* n__g1(31) -> 32* n__g1(33) -> 34* n__f1(15) -> 16* n__f1(17) -> 18* n__f1(9) -> 10* n__f1(23) -> 24* n__a2() -> 76* n__g2(73) -> 74* f0(2) -> 5* f0(4) -> 5* f0(1) -> 5* f0(3) -> 5* n__f2(69) -> 70* a0() -> 7* c2(79) -> 80* c0(2) -> 1* c0(4) -> 1* c0(1) -> 1* c0(3) -> 1* n__f0(2) -> 2* n__f0(4) -> 2* n__f0(1) -> 2* n__f0(3) -> 2* n__g0(2) -> 3* n__g0(4) -> 3* n__g0(1) -> 3* n__g0(3) -> 3* n__a0() -> 4* g0(2) -> 6* g0(4) -> 6* g0(1) -> 6* g0(3) -> 6* activate0(2) -> 8* activate0(4) -> 8* activate0(1) -> 8* activate0(3) -> 8* 1 -> 8,55,31,15 2 -> 8,46,39,23 3 -> 8,57,25,9 4 -> 8,49,33,17 10 -> 5* 16 -> 5* 18 -> 5* 24 -> 5* 26 -> 6* 32 -> 6* 34 -> 6* 40 -> 6* 41 -> 7* 46 -> 47* 47 -> 69,63 48 -> 47,63,8 49 -> 50,47 50 -> 47* 55 -> 56,47 56 -> 47* 57 -> 58* 58 -> 47* 63 -> 73* 64 -> 58,47,63,8 65 -> 50,47,63,8 70 -> 79,48,8 74 -> 64,8 76 -> 65,8 80 -> 48,8,47,73 problem: Qed